'''
Created on 14 jan 2010

@author: rlindeman
'''

import nltk

class ProverWrapper:
    """
        This class is a wrapper around the nltk.ParallelProverBuilderCommand class.
    """
    
    def __init__(self):
        """
            Initialize the nltk.ParallelProverBuilderCommand
        """
        prover9 = nltk.Prover9()
        mace = nltk.Mace()
        self.pprover = nltk.ParallelProverBuilderCommand(prover9, mace)
    
    def add_expression_assumptions(self, assumptions):
        """
            @type assumptions: C{list} of L{logic.Expression}
        """
        self.pprover.add_assumptions(assumptions)
        
    def add_string_assumptions(self, assumptions):
        """
            Parses each string in the list of assumptions as a LogicExpression
            and add the expression to the internal prover.
            @type assumptions: C{list} of L{string}
        """
        lp = nltk.LogicParser()
        assumption_expressions = []
        for assumption in assumptions:
            assumption_expression = lp.parse(assumption)
            assumption_expressions.append(assumption_expression)
        self.add_logic_assumptions(assumption_expressions)
            
    def set_expression_goal(self, goal):
        self.pprover._goal = goal

    def set_string_goal(self, goal):
        lp = nltk.LogicParser()
        goal_expression = lp.parse(goal)
        self.set_expression_goal(goal_expression)
        
    def prove(self, verbose=False):
        return self.pprover.prove(verbose)
    